* Step 1: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
e1(x1,x1,x,y,z,a()) -> e5(x1,x,y,z)
e2(x,x,y,z,z,a()) -> e6(x,y,z)
e2(i(),x,y,z,i(),a()) -> e6(x,y,z)
e3(x,y,x,y,y,z,y,z,x,y,z,a()) -> e6(x,y,z)
e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w)
e4(x,x,x,x,x,x,x,x,x,x,x,a()) -> e6(x,x,x)
e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> e5(x1,x,y,z)
e5(i(),x,y,z) -> e6(x,y,z)
f1(x,a()) -> g2(x,x)
f1(a(),x) -> g1(x,x)
f2(x,a()) -> g2(x,x)
f2(a(),x) -> g1(x,x)
g1(x,a()) -> h2(x)
g1(a(),x) -> h1(x)
g2(x,a()) -> h2(x)
g2(a(),x) -> h1(x)
h1(a()) -> i()
h2(a()) -> i()
- Signature:
{e1/6,e2/6,e3/12,e4/12,e5/4,f1/2,f2/2,g1/2,g2/2,h1/1,h2/1} / {a/0,e6/3,i/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {e1,e2,e3,e4,e5,f1,f2,g1,g2,h1,h2} and constructors {a,e6
,i}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
e1#(x1,x1,x,y,z,a()) -> c_1(e5#(x1,x,y,z))
e2#(x,x,y,z,z,a()) -> c_2()
e2#(i(),x,y,z,i(),a()) -> c_3()
e3#(x,y,x,y,y,z,y,z,x,y,z,a()) -> c_4()
e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w))
e4#(x,x,x,x,x,x,x,x,x,x,x,a()) -> c_6()
e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> c_7(e5#(x1,x,y,z))
e5#(i(),x,y,z) -> c_8()
f1#(x,a()) -> c_9(g2#(x,x))
f1#(a(),x) -> c_10(g1#(x,x))
f2#(x,a()) -> c_11(g2#(x,x))
f2#(a(),x) -> c_12(g1#(x,x))
g1#(x,a()) -> c_13(h2#(x))
g1#(a(),x) -> c_14(h1#(x))
g2#(x,a()) -> c_15(h2#(x))
g2#(a(),x) -> c_16(h1#(x))
h1#(a()) -> c_17()
h2#(a()) -> c_18()
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
e1#(x1,x1,x,y,z,a()) -> c_1(e5#(x1,x,y,z))
e2#(x,x,y,z,z,a()) -> c_2()
e2#(i(),x,y,z,i(),a()) -> c_3()
e3#(x,y,x,y,y,z,y,z,x,y,z,a()) -> c_4()
e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w))
e4#(x,x,x,x,x,x,x,x,x,x,x,a()) -> c_6()
e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> c_7(e5#(x1,x,y,z))
e5#(i(),x,y,z) -> c_8()
f1#(x,a()) -> c_9(g2#(x,x))
f1#(a(),x) -> c_10(g1#(x,x))
f2#(x,a()) -> c_11(g2#(x,x))
f2#(a(),x) -> c_12(g1#(x,x))
g1#(x,a()) -> c_13(h2#(x))
g1#(a(),x) -> c_14(h1#(x))
g2#(x,a()) -> c_15(h2#(x))
g2#(a(),x) -> c_16(h1#(x))
h1#(a()) -> c_17()
h2#(a()) -> c_18()
- Weak TRS:
e1(x1,x1,x,y,z,a()) -> e5(x1,x,y,z)
e2(x,x,y,z,z,a()) -> e6(x,y,z)
e2(i(),x,y,z,i(),a()) -> e6(x,y,z)
e3(x,y,x,y,y,z,y,z,x,y,z,a()) -> e6(x,y,z)
e3(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> e4(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w)
e4(x,x,x,x,x,x,x,x,x,x,x,a()) -> e6(x,x,x)
e4(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> e5(x1,x,y,z)
e5(i(),x,y,z) -> e6(x,y,z)
f1(x,a()) -> g2(x,x)
f1(a(),x) -> g1(x,x)
f2(x,a()) -> g2(x,x)
f2(a(),x) -> g1(x,x)
g1(x,a()) -> h2(x)
g1(a(),x) -> h1(x)
g2(x,a()) -> h2(x)
g2(a(),x) -> h1(x)
h1(a()) -> i()
h2(a()) -> i()
- Signature:
{e1/6,e2/6,e3/12,e4/12,e5/4,f1/2,f2/2,g1/2,g2/2,h1/1,h2/1,e1#/6,e2#/6,e3#/12,e4#/12,e5#/4,f1#/2,f2#/2,g1#/2
,g2#/2,h1#/1,h2#/1} / {a/0,e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1
,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1#
,h2#} and constructors {a,e6,i}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
e1#(x1,x1,x,y,z,a()) -> c_1(e5#(x1,x,y,z))
e2#(x,x,y,z,z,a()) -> c_2()
e2#(i(),x,y,z,i(),a()) -> c_3()
e3#(x,y,x,y,y,z,y,z,x,y,z,a()) -> c_4()
e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w))
e4#(x,x,x,x,x,x,x,x,x,x,x,a()) -> c_6()
e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> c_7(e5#(x1,x,y,z))
e5#(i(),x,y,z) -> c_8()
f1#(x,a()) -> c_9(g2#(x,x))
f1#(a(),x) -> c_10(g1#(x,x))
f2#(x,a()) -> c_11(g2#(x,x))
f2#(a(),x) -> c_12(g1#(x,x))
g1#(x,a()) -> c_13(h2#(x))
g1#(a(),x) -> c_14(h1#(x))
g2#(x,a()) -> c_15(h2#(x))
g2#(a(),x) -> c_16(h1#(x))
h1#(a()) -> c_17()
h2#(a()) -> c_18()
* Step 3: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
e1#(x1,x1,x,y,z,a()) -> c_1(e5#(x1,x,y,z))
e2#(x,x,y,z,z,a()) -> c_2()
e2#(i(),x,y,z,i(),a()) -> c_3()
e3#(x,y,x,y,y,z,y,z,x,y,z,a()) -> c_4()
e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w))
e4#(x,x,x,x,x,x,x,x,x,x,x,a()) -> c_6()
e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> c_7(e5#(x1,x,y,z))
e5#(i(),x,y,z) -> c_8()
f1#(x,a()) -> c_9(g2#(x,x))
f1#(a(),x) -> c_10(g1#(x,x))
f2#(x,a()) -> c_11(g2#(x,x))
f2#(a(),x) -> c_12(g1#(x,x))
g1#(x,a()) -> c_13(h2#(x))
g1#(a(),x) -> c_14(h1#(x))
g2#(x,a()) -> c_15(h2#(x))
g2#(a(),x) -> c_16(h1#(x))
h1#(a()) -> c_17()
h2#(a()) -> c_18()
- Signature:
{e1/6,e2/6,e3/12,e4/12,e5/4,f1/2,f2/2,g1/2,g2/2,h1/1,h2/1,e1#/6,e2#/6,e3#/12,e4#/12,e5#/4,f1#/2,f2#/2,g1#/2
,g2#/2,h1#/1,h2#/1} / {a/0,e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1
,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1#
,h2#} and constructors {a,e6,i}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph
1:S:e1#(x1,x1,x,y,z,a()) -> c_1(e5#(x1,x,y,z))
-->_1 e5#(i(),x,y,z) -> c_8():8
2:S:e2#(x,x,y,z,z,a()) -> c_2()
3:S:e2#(i(),x,y,z,i(),a()) -> c_3()
4:S:e3#(x,y,x,y,y,z,y,z,x,y,z,a()) -> c_4()
5:S:e3#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w) -> c_5(e4#(x1,x1,x2,x2,x3,x3,x4,x4,x,y,z,w))
-->_1 e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> c_7(e5#(x1,x,y,z)):7
-->_1 e4#(x,x,x,x,x,x,x,x,x,x,x,a()) -> c_6():6
6:S:e4#(x,x,x,x,x,x,x,x,x,x,x,a()) -> c_6()
7:S:e4#(i(),x1,i(),x1,i(),x1,i(),x1,x,y,z,a()) -> c_7(e5#(x1,x,y,z))
-->_1 e5#(i(),x,y,z) -> c_8():8
8:S:e5#(i(),x,y,z) -> c_8()
9:S:f1#(x,a()) -> c_9(g2#(x,x))
-->_1 g2#(a(),x) -> c_16(h1#(x)):16
-->_1 g2#(x,a()) -> c_15(h2#(x)):15
10:S:f1#(a(),x) -> c_10(g1#(x,x))
-->_1 g1#(a(),x) -> c_14(h1#(x)):14
-->_1 g1#(x,a()) -> c_13(h2#(x)):13
11:S:f2#(x,a()) -> c_11(g2#(x,x))
-->_1 g2#(a(),x) -> c_16(h1#(x)):16
-->_1 g2#(x,a()) -> c_15(h2#(x)):15
12:S:f2#(a(),x) -> c_12(g1#(x,x))
-->_1 g1#(a(),x) -> c_14(h1#(x)):14
-->_1 g1#(x,a()) -> c_13(h2#(x)):13
13:S:g1#(x,a()) -> c_13(h2#(x))
-->_1 h2#(a()) -> c_18():18
14:S:g1#(a(),x) -> c_14(h1#(x))
-->_1 h1#(a()) -> c_17():17
15:S:g2#(x,a()) -> c_15(h2#(x))
-->_1 h2#(a()) -> c_18():18
16:S:g2#(a(),x) -> c_16(h1#(x))
-->_1 h1#(a()) -> c_17():17
17:S:h1#(a()) -> c_17()
18:S:h2#(a()) -> c_18()
The dependency graph contains no loops, we remove all dependency pairs.
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{e1/6,e2/6,e3/12,e4/12,e5/4,f1/2,f2/2,g1/2,g2/2,h1/1,h2/1,e1#/6,e2#/6,e3#/12,e4#/12,e5#/4,f1#/2,f2#/2,g1#/2
,g2#/2,h1#/1,h2#/1} / {a/0,e6/3,i/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/1,c_6/0,c_7/1,c_8/0,c_9/1,c_10/1,c_11/1
,c_12/1,c_13/1,c_14/1,c_15/1,c_16/1,c_17/0,c_18/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {e1#,e2#,e3#,e4#,e5#,f1#,f2#,g1#,g2#,h1#
,h2#} and constructors {a,e6,i}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(1))